(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basics/relations.ma".
include "basics/lists/list.ma".     

(*This is a stupid example, but there are more complex and useful example like this*)
inductive bad_type :Type[0] ≝ (*Inductive type using list, does induction work?*)
  | lbase :bad_type
  | L : (list bad_type) → bad_type. 
   
   
(*This is what I expect as induction*)

(* theorem induction_bad_type_right : (*unprovable theorem, comment to go on*)
∀p:bad_type→ Prop.
  p lbase → (p (L [ ])) → (∀h.p h → ∀l.p (L l) → p (L (h::l))) → ∀b.p b.

  #P
  #B
  #BL
  #I
  #T
  elim T
  [
    @B (*This works because of the base hypothesis*)
  | #LT elim LT
    [ @BL (*This works because of the base hypothesis AND the induction on the empty list*)
    | #H #TL
      #IND
      @I //
       (*I don't have any hypothesis on H, but H is smaller than T*)
   //
*)

  
(*This is what "elim" gives*)
            
theorem induction_bad_type_wrong : 
  ∀p:bad_type→ Prop.
    p lbase → (p (L [ ])) → (∀l.∀h.p (L l) → p (L (h::l))) → ∀b.p b.
    #P
    #B
    #BL
    #I
    #T
    elim T
    [ @B
    | #LT elim LT 
        [ @BL
        | #H #TL 
          #IND
          @I @IND ]]qed.   


(*Is this induction all that we need?
  Let's try an example*)
  
let rec always_True b ≝  
    match b with [ 
      lbase ⇒  True
    |  L l ⇒  (All ? always_True l)]. (* All gives True if l=[]) *)
    


let rec size b ≝
  match b with [
      lbase ⇒ 0
   |  L l ⇒  \fold[plus,1]_{i∈l} (size i)].


theorem t1 : ∀b.always_True b.
#b cut (∃n. size b =n) [%{(size b)} //] * #n lapply b -b
@(nat_elim1 n) -n #m #H #b cases b
[ //
|#l cases l normalize //
 #b1 #l1 #H1 %
  [@(H … (refl …)) <H1 >(plus_n_O (size b1)) in ⊢ (?%?); whd
   >(plus_n_Sm (size b1) 0) in ⊢ (?%?); @monotonic_le_plus_r
   elim l1 // #a #tl normalize /2/
  |lapply(sym_eq nat …H1) >commutative_plus -H1 #H1 lapply (eq_plus_to_le … H1)
   -H1 elim l1 //
   #b2 #l2 #Hind normalize #H1 %
    [@(H … (refl …)) @(lt_to_le_to_lt … H1) >(plus_n_O (size b2)) in ⊢ (?%?); whd
     >(plus_n_Sm (size b2) 0) in ⊢ (?%?); @monotonic_le_plus_r
     elim l2 // #a #tl normalize /2/
    |@Hind /2/
    ]
  ]
]
qed.
(* theorem t1 : ∀b. always_True b = True. (*unprovable theorem, comment to go on*)

  #B elim B
  //
  #LIS
  elim LIS
  normalize // 
  #H #TL
  #IND
  >IND
    (*Now? H is totally free.*) *)
  

(*Let's try the induction lemma *)

(* theorem t2 : ∀b. always_True b = True. (*unprovable theorem, comment to go on*)

  #B @(induction_bad_type_wrong (λb. always_True b =True))
  [ //
  | normalize //
  | #TL #H normalize #IND >IND (*It's the same as elim!*) *)


(* The problem is even in let rec construction *)

let rec my_fun_wrong (b:list bad_type) ≝ 
  match b with [
    nil ⇒ True
  | cons h tl ⇒ match h with [ 
      lbase ⇒ True
    | L l ⇒ (my_fun_wrong l) ∧ (my_fun_wrong tl) (*But l is smaller!*)
    ]
].
